Nuprl Lemma : iflift_1 4,23

AB:Type, c:f:(AB), xy:Af(if c x else y fi) = if c f(x) else f(y) fi 
latex


DefinitionsUnit, P  Q, P & Q, P  Q, Prop, , b, A, b, x:AB(x), t  T, x(s)
Lemmasassert wf, not wf, bnot wf, bool wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert

origin